(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(x1) → b(x1)
b(b(b(c(x1)))) → c(c(a(a(b(a(x1))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:

A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(a(b(a(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
S tuples:

A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(a(b(a(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace B(b(b(c(z0)))) → c2(A(a(b(a(z0)))), A(b(a(z0))), B(a(z0)), A(z0)) by

B(b(b(c(x0)))) → c2(A(b(b(a(x0)))), A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:

A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(A(b(b(a(x0)))), A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
S tuples:

A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(A(b(b(a(x0)))), A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace B(b(b(c(x0)))) → c2(A(b(b(a(x0)))), A(b(a(x0))), B(a(x0)), A(x0)) by

B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:

A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
S tuples:

A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2, c2

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0)) by

B(b(b(c(x0)))) → c2(A(b(b(b(x0)))), A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:

A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
S tuples:

A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2, c2, c2

(9) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0)) by B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:

A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
S tuples:

A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2, c2, c2

(11) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace B(b(b(c(x0)))) → c2(A(b(a(x0)))) by B(b(b(c(z0)))) → c2(A(b(b(z0))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:

A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
S tuples:

A(z0) → c1(B(z0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2, c2, c2

(13) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace B(b(b(c(x0)))) → c2(A(b(b(b(x0)))), A(b(a(x0))), B(a(x0)), A(x0)) by B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:

A(z0) → c1(B(z0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
S tuples:

A(z0) → c1(B(z0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

A, B

Compound Symbols:

c1, c2, c2, c2

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A(z0) → c1(B(z0)) by

A(b(b(c(b(c(y0)))))) → c1(B(b(b(c(b(c(y0)))))))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:

B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
A(b(b(c(b(c(y0)))))) → c1(B(b(b(c(b(c(y0)))))))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
S tuples:

B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
A(b(b(c(b(c(y0)))))) → c1(B(b(b(c(b(c(y0)))))))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:

B, A

Compound Symbols:

c2, c2, c2, c1

(17) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
A(b(b(c(b(c(y0)))))) → c1(B(b(b(c(b(c(y0)))))))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

a, b

Defined Pair Symbols:none

Compound Symbols:none

(19) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(20) BOUNDS(O(1), O(1))